$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, ${\it upd}$:update{-}spec(${\it ds}$;${\it da}$), $k$:Knd, $x$:Id.
\\[0ex]update{-}spec{-}dom(${\it upd}$;$k$;$x$) $\in$ $\mathbb{B}$